Inference at * 
Iof proof for Lemma do-apply-compose':


  A, B, C:Type, g:(A(B + Top)), f:(ABC), x:A.
  (can-apply(f o' g;x))  (do-apply(f o' g;x) ~ (f(x,do-apply(g;x)))) 

latex

 by (((UnivCD) 
CollapseTHENA (Auto)) 
CollapseTHEN (MoveToConcl (-1))) 
CollapseTHEN ((
CRepUR ``do-apply can-apply p-compose\'`` ( 0)) 
CollapseTHEN (((GenConclAtAddr [1;1;1;1;1]) 

CoCollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto
C))))) 

latex

C.

Definitions	Type, f o' g, can-apply(f;x), do-apply(f;x), f(a), s = t, x:A. B(x), x:AB(x), Top, left + right, True, b, P  Q, t  T, False
Lemmas	true wf, false wf